Nuprl Definition : R-occurs
11,40
postcript
pdf
R-occurs(
R
;
i
;
z
)
== es_realizer_ind(
R
;
== es_realizer_ind(
ff;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.bor(
rec1
;
rec2
);
== es_realizer_ind(
loc
,
T
,
x
,
v
.band(eq_id(
loc
;
i
); eq_id(
z
;
x
));
== es_realizer_ind(
loc
,
T
,
x
,
L
.band(eq_id(
loc
;
i
); eq_id(
z
;
x
));
== es_realizer_ind(
lnk
,
tag
,
L
.ff;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.band(eq_id(
loc
;
i
); bor(eq_id(
z
;
x
); fpf-dom(id-deq;
z
;
ds
)));
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.band(eq_id(source(
l
);
i
); fpf-dom(id-deq;
z
;
ds
));
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.band(eq_id(
loc
;
i
); fpf-dom(id-deq;
z
;
ds
));
== es_realizer_ind(
loc
,
k
,
L
.band(eq_id(
loc
;
i
); deq-member(id-deq;
z
;
L
));
== es_realizer_ind(
loc
,
k
,
L
.ff;
== es_realizer_ind(
loc
,
x
,
L
.band(eq_id(
loc
;
i
); eq_id(
z
;
x
)))
latex
Definitions
eq_id(
a
;
b
)
,
band(
p
;
q
)
,
ff
,
id-deq
,
deq-member(
eq
;
x
;
L
)
,
fpf-dom(
eq
;
x
;
f
)
,
source(
l
)
,
bor(
p
;
q
)
,
es
realizer
ind
FDL editor aliases
R-occurs
origin